es:ES, x:Id, e:{e:E| @loc(e)(x:)} .
((x when e) = tt  )
 ((x initially@loc(e)  = ff  )  (e':E. (e' loc e  & (x when e') = ff  )))
 (e':E
 (((e' <loc e)
 (& (x when e') = ff  
 (& (x after e') = tt  
 (& e''(e',e].(x when e'') = tt  
 (& e''[e',e).(x after e'') = tt  )) 

latex

Definitions	x:A. B(x), x:AB(x), ES, Id, E, , @i(x:T), {x:A| B(x)} , s = t, e loc e' , x:A  B(x), P & Q, x:A. B(x), left + right, P  Q, (e <loc e'), e(e1,e2].P(e), e[e1,e2).P(e), P  Q, tt
Lemmas	es-lc-bool